perm filename CONTEX[W86,JMC] blob sn#812596 filedate 1986-03-16 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Contexts and Mental Situations
C00012 ENDMK
C⊗;
Contexts and Mental Situations

Here are two ideas that may later be combined, but I don't
think it would be a good idea to do that now.

Contexts

Understanding a sentence, whether it is in natural language
or is a logic sentence used by a program depends on "knowing" the
context in which it is asserted.  If this is built into the program,
then it is difficult combine sentences with different contexts,
and the program is usually quite brittle.  Therefore, we propose
to represent the context explicitly in the sentence and write
holds(on(x,y),c)  instead of just  on(x,y).  The context  c  will
always be incompletely prescribed.  Two people or two programs
may adjust contexts explicitly in order to mean the same thing
by certain formulas or terms, but a third person may have to
make further explicit presumptions in order to adjust to them,
because these presumptions are implicit in the conversation of
the first two.  Part of the intent in introducing contexts is
to achieve elaboration tolerance.  In so far as particular
domains, e.g. some kind of blocks world, are described by
axioms involving delimited contexts, we can give other axioms
valid in other contexts without contradiction.  However, we
hope to be able some of the value of a delimited axiom
system by non-monotonically inferring that certain sentences
true in a context also hold in more general contexts.

  Perhaps we have formulas like

holds(holds(p,c1),c2)

or value(value(<term>,c1),c2).

Note: the(Cat,c1) denotes the cat referred to as "the cat"
in context  c1.

Note:  We may sometimes use a (generalized) syntactic sugaring in which
the system "enters" a context  c.  Then the system can
use the formula  on(Cat,Mat),  but this involves temporarily
changing the status of  on(Cat,Mat)  from term to formula.

The context  c  may include time, place, identification
of what  x  and  y  stand for, story, etc.  More generally it
includes whatever might be implicit when a human says  on(x,y)
as in  on(Cat,Mat).

Note: The use of  Now  for controlling reasoning may somehow be
mergeable into contexts.

There are operators on contexts:  time(t,c)  is a modification
of  c  in which the time is specificed to be  t.  We may also
have  time1(p,t)  which is an assertion that the sentence  p
is true at time  t.  We then have the trade-off axiom

holds(p,time(t,c)) iff holds(time1(p,t),c).

We can also use situations instead of times, and this might
be a convenient way to get situations in.

There is a relation of relative explicitness among contexts,
written  c1 < c2.  We have

holds(p,c2) and c1 < c2 implies  holds(p,c1)

and the non-monotonic upwards inheritance axiom

holds(p,c1) and c1 < c2 and not ab aspectx(p,c1,c2) implies holds(p,c2).
We may also have

time(t,c) <= c

provided we wish to consider  time(t,c) = c  when  c  already is
explicit about the time.

We also need to consider operations that modify contexts, but
then we have to decide what to do about the frame problem.

Contexts relevant to the blocks world

We may have Cbw1 as a specific blocks world context.  However,
writing axioms requires something like a predicate  bw0(c)
prescribing a certain kind of blocks world context about which
we can write axioms.  One way of writing such axioms might be

∀ c.bw0(c) ⊃ (∀ s x e.¬ab aspect1(x,e,s,c)
⊃ loc(x,result(e,s,c),c),c) = loc(x,s,c)),

but it is unpleasant and perhaps avoidable to have situations
and contexts in all these functions and predicates.  We can
perhaps get by with only contexts if we imagine that certain
contexts incorporate situations.  Consider

∀ c.bw1 c ∧ ¬ab aspect1(x,e,c) ⊃ loc(x,result(e,c)) = loc(x,c).

Here we have absorbed the situation into the context and  result  gives
a new context.  We also have  bw1(c) ∧ okevent(e,c) ⊃ bw1(result(e,c)).

If  bw0(c), where this may not mean precisely the same as above,
no specific situation is prescribed.  Therefore,  aspect1(x,e,c),
result(e,c) and  loc(x,c)  are not meaningful.  However, we may
have something like

bw0(c) ∧ oksit(s,c) ⊃ bw1(prescribe(s,c))
 ∧  situation(prescribe(s,c))=s.


Mental situation calculus

Mental situations include beliefs, goals and intentions
and may include physical situations.  Mental events, including
actions and observations, change mental situations.  Suitable
axioms analogous to those of ordinary situation calculus
describe the effects of mental events.  An important
predicate is  should(s,a)  meaning that in the mental
situation  s  the thinker should do action  a, where  a
is either mental or physical.

1985 Mar 16

More natural deduction (i.e. more natural than Gentzen's)

	The human use of contexts may be like the use of premisses
in natural deduction.  Suppose we make a context logic that looks
as follows:

1. We have a statement

holds(p,c)

2. Replacing assumption we have the act of entering a context.  For
example

enter c

If we have  holds(p,c) and we enter  c,  we may write

p

Now suppose we deduce  q  by predicate calculus (actually predicate
calculus supplemented by the rule we are about to introduce).
Now we may discharge the context  c,  and write

holds(q,c).

Ordinary natural deduction would begin with  (c ⊃ p) and assume c,
then deduce  q  and discharge the assumption to get  (c ⊃ q).
Our contextual natural deduction is weaker.

An example:

holds(1960,at(jmc,mit))
holds(1960,at(suppes,Stanford))
(enter 1960)
at(jmc,mit)
at(suppes,Stanford)

<steps using these and other assumptions>

¬colleagues(jmc,Suppes)

holds(1960,¬colleagues(jmc,Suppes))

Now if we add holds(1963,at(jmc,Stanford))
and holds(1963,at(Suppes,Stanford))

then our ultra-natural deduction permits us to deduce

holds(1963,colleagues(jmc,Suppes)).

I wonder if contextual natural deduction is anything like natural
deduction in some modal logics.